$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $x$:ecl(${\it ds}$;${\it da}$), $L$:event{-}info(${\it ds}$;${\it da}$) List.
\\[0ex]ecl{-}halt(${\it ds}$;${\it da}$;$x$)(0,$L$) $\Rightarrow$ 2of(2of(last($L$))) $\in$ ecl{-}halt{-}type(${\it da}$;$x$)